#!/usr/bin/python

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL


rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 50
for i in range(0,maxPrio):
  rank.append([])


if lemma == "helpingUpdateKey":
  # only prioritize ReaderK() and TagK() goals and then full auto mode
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*ReaderK\(.*', line):
      rank[30].append(num)
    elif re.match('.*TagK\(.*', line):
      rank[20].append(num)
    else:
      rank[5].append(num)

elif lemma == "helpingOutNotKey":
  # !Tag and !Reader facts
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)

    if (re.match('.*!Tag\(.*', line) or
        re.match('.*!Reader\(.*', line) or
        re.match('.*ReaderState1\(.*', line)):
      rank[9].append(num)
    elif re.match('.*TagK\(.*', line):
      rank[4].append(num)
    else:
      rank[5].append(num)


elif lemma == "helpingSecrecy" or lemma == "noninjectiveagreementTAG":
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)

    if lemma == "noninjectiveagreementTAG":
      if (re.match('.*Running\(.*', line) or
          re.match('.*splitEqs\(7.*', line)):
        rank[47].append(num)
      elif (re.match('.*!K.\(.*x\.1.*', line)):
        rank[46].append(num)

    if re.match('.*~~>.*', line):
      rank[48].append(num)
    if (re.match('.*!KU\( ~k.*', line)):
      rank[46].append(num)
    elif (re.match('.*!KU\( h\(~k.*', line)):
      rank[44].append(num)
    elif (re.match('.*!KU\( h\(k0\).*', line) or
          re.match('.*!KU\( h\(h\(k0', line)):
      rank[42].append(num)
    elif (re.match('.*!K.\(.*r1\.1.*', line) or
          re.match('.*!K.\(.*r1.*', line) or
          re.match('.*!K.\(\(.*z1\.1.*', line) or
          re.match('.*!K.\(\(.*z1.*', line) or
          re.match('.*!K.\(\(.*~r0\.1.*', line) or
          re.match('.*!K.\(\(.*~r0.*', line) or
          re.match('.*!K.\( \(.*~r0\.1.*', line) or
          re.match('.*!K.\( \(.*~r0.*', line) or
          re.match('.*!K.\( ~r.*', line) or
          re.match('.*!K.\( \(z.1', line) or
          re.match('.*!K.\( \(h\(k0.*h\(.*', line) or
          re.match('.*!K.\(.*x.*h.*', line)):          
      rank[40].append(num)
    elif (re.match('.*!KU\(.*r1\.1.*', line) or
          re.match('.*!KU\(.*r1.*', line)):
      rank[35].append(num)
    elif (re.match('.*!Tag\(.*', line) or
          re.match('.*!Reader\(.*', line) or
          re.match('.*ReaderState1\(.*', line) or
          re.match('.*TagState1\(.*', line)):
      rank[30].append(num)
    elif (re.match('.*ReaderState1\(.*', line) or
          re.match('.*TagState1\(.*', line)):
      rank[27].append(num)
    elif (re.match('.*!K.\( \(x.*h\(k0', line)):
      rank[22].append(num)
    elif (re.match('.*splitEqs\(2\.*', line)):
      rank[17].append(num)
    elif (re.match('.*splitEqs\(3\.*', line)):
      rank[15].append(num)
    elif (re.match('.*!KU\( ~k.*', line)):
      rank[46].append(num)
    else:
      rank[5].append(num)


elif lemma == "noninjectiveagreementREADER":
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*Update\(.*', line):
      rank[0].append(num)
    else:
      rank[5].append(num)
  
elif lemma == "executable":
  # only prioritize ReaderK() and TagK() goals and then full auto mode
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*Update\(.*', line):
      rank[0].append(num)
    else:
      rank[5].append(num)

else:
  if debug:
    sys.stderr.write("No lemma found")
  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    if debug:
      sys.stderr.write(goal)
      print goal

